T:Type, x, y, u:T, L:(T List).
adjacent(T;[u / L];x;y)  ((0 < ||L||) & ((x = u & y = hd(L))  adjacent(T;L;x;y))) 

latex

ProofTree

Definitions

i  j , ||as||, {i..j}, s = t, x:A  B(x), P & Q, x:A. B(x), Type, type List, a < b, left + right, P  Q, , {x:A| B(x)} , t  T, #$n, , A c B, n+m, l[i], , n - m, hd(l), [car / cdr], x:AB(x), P  Q, P  Q, x:A. B(x), <a, b>, False, A, A  B, i  j < k, Dec(P), P  Q, Atom, b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, f(a), x f y, |r|, xL. P(x), (xL.P(x)), x:A.B(x), x. t(x), (x  l), adjacent(T;L;x;y), {T}, SQType(T), s ~ t, i <z j, i z j, tl(l), -n, Void, , True, T, []

Lemmas

length wf1, true wf, squash wf, select cons tl, nat wf, member wf, le wf, decidable int equal, guard wf, iff wf, decidable ex int seg, decidable cand, select wf, rev implies wf, int seg wf